FDL - Nuprl Definition : strongwellfounded

Nuprl Definition : strongwellfounded

11,40

SWellFounded(R(x;y)) ==

f:T

. (

x,y:T. R(x;y)

((f(x)) < (f(y))))

clarification:

strongwellfounded(T; x,y.R(x;y)) ==

f:T

. (

x:T, y:T. R(x;y)

((f(x)) < (f(y))))

Definitions x:A. B(x), x:AB(x), , x:A. B(x), P Q, a < b, f(a)

FDL editor aliases strongwellfounded

Definitions	x:A. B(x), x:AB(x), , x:A. B(x), P Q, a < b, f(a)
FDL editor aliases	strongwellfounded